g:IMonoid, b:, p:|g|. (when b. p)  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid, when b. p
Definitions	when b. p, t  T, x:A. B(x), IMonoid
Lemmas	imon wf, bool wf, grp id wf, grp car wf, ifthenelse wf